(***************************************************************************
 * Cast-Free Featherweight Java
 *
 * Bruno De Fraine, with help from Erik Ernst and Mario Sudholt, Summer 2008
 ***************************************************************************)

(** printing \in %\ensuremath{\in}% *)
(** printing \notin %\ensuremath{\notin}% *)
(** printing == %\ensuremath{\doteq}% *)

Require Import Metatheory.

(** * Syntax *)
Definition var := atom.		(* variable name *)
Definition fieldname := atom.	(* field name *)
Definition mname := atom.	(* method name *)
Definition scname := atom.	(* simple class name *)
Definition tvname := atom.	(* type var name *)

Inductive type : Set :=
| t_C : scname -> type
| t_X : tvname -> type
| t_CdotC : scname -> scname -> type
| t_XdotC : tvname -> scname -> type
| t_dotC : scname -> type.

Hint Constructors type.

Inductive typeis_famname : type -> Prop := (* subset of type *)
| tif_C : forall C,
    typeis_famname (t_C C)
| tif_X : forall X,
    typeis_famname (t_X X).

Hint Constructors typeis_famname.

Inductive typeis_qcname : type -> Prop := (* subset of type *)
| tiq_C : forall C,
    typeis_qcname (t_C C)
| tiq_CdotC : forall C D,
    typeis_qcname (t_CdotC C D).

Hint Constructors typeis_qcname.

Inductive typesare_famname : list type -> Prop :=
| taf_nil : 
    typesare_famname nil
| taf_cons : forall t ts,
    typeis_famname t ->
    typesare_famname (t::ts).

Hint Constructors typesare_famname.

Inductive typeis_nested : type -> Prop :=
| tin1 : forall C D : scname, typeis_nested (t_CdotC C D)
| tin2 : forall X D : scname, typeis_nested (t_XdotC X D)
| tin3 : forall C : scname, typeis_nested (t_dotC C).

Hint Constructors typeis_nested.

Inductive typeis_top : type -> Prop :=
| tit1 : forall C : scname, typeis_top (t_C C)
| tit2 : forall X : scname, typeis_top (t_X X).

Hint Constructors typeis_top.

Inductive exp : Set :=
| e_var : var -> exp
| e_field : exp -> fieldname -> exp
| e_meth : exp -> mname ->
           list type -> list exp -> exp
| e_new : type -> list exp -> exp.

Hint Constructors exp.

Definition exp_ind2' :=
  fun (P:exp->Prop) (Q:list exp->Prop)
      (f : forall v : var, P (e_var v))
      (f0 : forall e : exp, P e -> forall f0 : fieldname, P (e_field e f0))
      (f1 : forall (e:exp) (m : mname) (l : list type) (l0 : list exp),
              P e -> Q l0 -> P (e_meth e m l l0))
      (f2 : forall (t : type) (l : list exp), Q l -> P (e_new t l))
      (f3 : Q nil)
      (f4 : forall e l, P e -> Q l -> Q (e :: l)) =>
    fix F (e:exp) : P e :=
  match e as e0 return (P e0) with
    | e_var v => f v
    | e_field e0 f3 => f0 e0 (F e0) f3
    | e_meth e0 m l l0 => f1 e0 m l l0 (F e0) 
                          ((list_ind Q f3 (fun (e:exp) (l:list exp) =>
                                             (f4 e l (F e)))) l0)
    | e_new t l => f2 t l ((list_ind Q f3 (fun (e:exp) (l':list exp) =>
                                             (f4 e l' (F e)))) l)
  end.

Lemma exp_ind2: 
  forall (P:exp->Prop),
    (forall v : var, P (e_var v)) ->
    (forall e : exp, P e -> forall f0 : fieldname, P (e_field e f0)) ->
    (forall (e:exp) (m : mname) (l : list type) (l0 : list exp), 
       P e -> (forall e', In e' l0 -> P e') -> P (e_meth e m l l0)) ->
    (forall (t : type) (l : list exp), 
       (forall e', In e' l -> P e') -> P (e_new t l)) ->
    forall (e:exp), P e.
Proof.
  intros.
  refine (exp_ind2' P (fun l0 => forall e', In e' l0 -> P e')
         H H0 H1 H2 _ _ _).
    intros.
    inversion H3.
  intros.
  inversion H5; subst.
    assumption.
  apply H4.
  assumption.
Qed.

(** * Environments *)
Definition benv := (list (tvname * scname)).
Definition senv := (list (var * exp)).
Definition tenv := (list (var * type)).

Definition fsin := (fieldname * type)%type.
Definition fenv := (list fsin).

Definition kenv := (scname * fenv)%type.

Definition msin := (mname * (benv * type * tenv * exp))%type.
Definition menv := (list msin).

Definition ncsin := (scname * (fenv * kenv * menv))%type.
Definition ncenv := (list ncsin).

Definition csin := (scname * (scname * fenv * kenv * menv * ncenv))%type.
Definition cenv := (list csin).

(** * Declarations *)
Definition fdecl := (type * fieldname)%type.
Definition fdecls := (list fdecl).
Definition kdecl := (scname * fdecls)%type.

Definition mdecl := (benv * type * mname * tenv * exp)%type.
Definition mdecls := (list mdecl).

Definition ncdecl := (scname * fdecls * kdecl * mdecls)%type.
Definition ncdecls := (list ncdecl).

Definition tcdecl := (scname * scname * fdecls * kdecl * 
                    mdecls * ncdecls)%type.

Definition cdecls := (list tcdecl).
(* Was ctable. This is the program which goes through 
   make_cenv to convert tcdecls (syntax) into a form
   more suitable for the semantics of the language. *)

(** * Parameters *)
Parameter CT : cenv.
Parameter this : var.
Parameter Object : scname.

(** * Auxiliaries *)
Definition fdecl2fsin (fs:fdecl) : fsin :=
  match fs with (T,fn) => (fn,T) end.

Definition kdecl2kenv (kd:kdecl) : kenv :=
  match kd with (C,fs) => (C,List.map fdecl2fsin fs) end.

Definition mdecl2msin (md:mdecl) : msin :=
  match md with (E,T,m,tE,e) => (m,(E,T,tE,e)) end.

Definition ncdecl2ncsin (nd:ncdecl) : ncsin :=
  match nd with (C,fs,k,ms) => 
    (C,(List.map fdecl2fsin fs, kdecl2kenv k, 
        List.map mdecl2msin ms)) end.

Definition cdecl2csin (cd:tcdecl) : csin :=
  match cd with  (C,D,fs,k,ms,ns) =>
    (C, (D, List.map fdecl2fsin fs, kdecl2kenv k,
         List.map mdecl2msin ms, List.map ncdecl2ncsin ns)) end.

Definition make_cenv (cds:cdecls) : cenv :=
  List.map cdecl2csin cds.

Hint Unfold fdecl2fsin kdecl2kenv mdecl2msin 
     ncdecl2ncsin cdecl2csin make_cenv.

Lemma no_binds_lemma :
  forall (A:Type) (x:atom) (v:A) E,
    no_binds x E ->
    ~ binds x v E.
Proof.
  intros.
  unfold binds.
  unfold no_binds in H.
  rewrite H.
  discriminate.
Qed.

Hint Resolve no_binds_lemma.

(* lookup field decls *)
Inductive fields : type -> fenv -> Prop :=
| f_tobject :
    fields (t_C Object) nil
| f_tclass : forall C D fs gs c ms ns,
    binds C (D,fs,c,ms,ns) CT ->
    fields (t_C D) gs ->
    fields (t_C C) (gs ++ fs)
| f_nobject_C : forall C,
    fields (t_CdotC Object C) nil
| f_nclass : forall C D E fs gs hs c c' ms ms' ns,
    binds C (D,hs,c,ms,ns) CT ->
    binds E (fs,c',ms') ns -> 
    fields (t_CdotC D E) gs ->
    fields (t_CdotC C E) (gs ++ fs)
| f_nsuper : forall C D E c fs gs ms ns,
    binds C (D,fs,c,ms,ns) CT ->
    no_binds E ns -> 
    fields (t_CdotC D E) gs ->
    fields (t_CdotC C E) gs.

Hint Constructors fields.

Definition field (C : type) (f : fieldname) (t : type) : Prop :=
    exists2 fs, fields C fs & binds f t fs.

Hint Unfold field.

(** * Typing *)
(** ** Well-formed types *)

(** [ok_type t A] holds when t is typeable in context A. *)

Inductive ok_type (env:benv) : type -> type -> Prop :=
| wf_object : forall A,
    ok_type env (t_C Object) A
| wf_ccls : forall C cd A,
    binds C cd CT ->
    ok_type env (t_C C) A
| wf_ncls : forall A C D E fs c ms ns cd,
    typeis_qcname A ->
    binds C (D,fs,c,ms,ns) CT -> 
    binds E cd ns ->
    ok_type env (t_CdotC C E) A
| wf_sncls : forall A C D E fs c ms ns,
    typeis_qcname A ->
    binds C (D,fs,c,ms,ns) CT ->
    no_binds E ns ->
    ok_type env (t_CdotC D E) A ->
    ok_type env (t_CdotC C E) A
| wf_var : forall X C A,
    binds X C env ->
    ok_type env (t_C C) A ->
    ok_type env (t_X X) A
| wf_absfam : forall X C D A,
    typeis_qcname A ->
    binds X D env ->
    ok_type env (t_CdotC D C) A ->
    ok_type env (t_XdotC X C) A
| wf_rel : forall E C D,
    ok_type env (t_CdotC C E) (t_CdotC C D) ->
    ok_type env (t_dotC E) (t_CdotC C D).

Hint Constructors ok_type.

(** ** Subtyping *)

(** [extends C D] holds if [C] is a direct subclass of [D]. *)
Definition extends (C D : scname) : Prop :=
  exists fs c ms ns,
    binds C (D,fs,c,ms,ns) CT.

Hint Unfold extends.

(** [sub E s u] holds if [s] is a subtype of [u] in bound environment E. 
The subtype relation is the reflexive, transitive closure of the direct subclass relation. *)
Inductive sub (env:benv) : type -> type -> Prop :=
  | s_refl : forall T,
      sub env T T
  | s_var : forall X C,
      binds X C env ->
      sub env (t_X X) (t_C C)
  | s_object : forall T,
      sub env T (t_C Object)
  | s_trans : forall S T U,
      sub env S T ->
      sub env T U ->
      sub env S U
  | s_class : forall C D fs c ms ns,
      binds C (D,fs,c,ms,ns) CT ->
      sub env (t_C C) (t_C D).

Hint Constructors sub.

(* method typing *)

Inductive method : mname -> type -> benv -> type -> tenv -> exp -> Prop :=
| mt_tclass : forall C D fs c ms ns m env tenv t e,
    binds C (D,fs,c,ms,ns) CT ->
    binds m (env,t,tenv,e) ms ->
    method m (t_C C) env t tenv e
| mt_tsuper : forall C D fs c m ms ns env tenv t e,
    binds C (D,fs,c,ms,ns) CT ->    
    no_binds m ms ->
    method m (t_C D) env t tenv e ->
    method m (t_C C) env t tenv e
| mt_nclass : forall C D fs c m ms ns E fs' c' ms' env tenv t e,
    binds C (D,fs,c,ms,ns) CT ->
    binds E (fs',c',ms') ns ->
    binds m (env,t,tenv,e) ms' ->
    method m (t_CdotC C E) env t tenv e
| mt_nsuper1 : forall C E D m fs fs' c c' ms ms' ns env tenv t e,
    binds C (D,fs,c,ms,ns) CT ->    
    binds E (fs',c',ms') ns ->
    no_binds m ms' ->
    method m (t_CdotC D E) env t tenv e ->
    method m (t_CdotC C E) env t tenv e
| mt_nsuper2 : forall C D E m fs c ms ns env tenv t e,
    binds C (D,fs,c,ms,ns) CT ->    
    no_binds E ns ->
    method m (t_CdotC D E) env t tenv e ->
    method m (t_CdotC C E) env t tenv e.

Hint Constructors method.

(** ** Term substitution *)

(** [subst_exp E e] returns the term expression [e] where any occurrences of bound variables have been replaced by their bindings in environment [E]. *)
Fixpoint subst_exp (E : senv) (e : exp) {struct e} : exp :=
    match e with
    | e_var v =>
        match get v E with
        | Some e' => e'
        | None => e_var v
        end
    | e_field e0 f => e_field (subst_exp E e0) f
    | e_meth e0 m Ps es => e_meth (subst_exp E e0) m Ps
                                   (List.map (subst_exp E) es)
    | e_new C es => e_new C (List.map (subst_exp E) es)
    end.

Hint Unfold subst_exp.

Definition subst_type' (XT:(tvname*type)) (t:type) : type :=
  match XT, t with
    | (X,t_C C), t_X Y => 
      if X == Y then t_C C else t
    | (X,t_C C), t_XdotC Y D => 
      if X == Y then t_CdotC C D else t
    | _, _ => t
  end.

Fixpoint subst_type (XTs:list (tvname*type)) (t:type) : type :=
  match XTs with
    | nil => t
    | XT :: XTs' => subst_type XTs' (subst_type' XT t)
  end.

Definition subst_types (XTs:list (tvname*type)) (ts:list type) : list type :=
  List.map (subst_type XTs) ts.

Fixpoint subst_type_exp (XTs:list (tvname*type)) (e:exp) : exp :=
  match e with
    | e_var _ => e
    | e_field e0 f => e_field (subst_type_exp XTs e0) f
    | e_meth e0 m Ps es => 
      e_meth (subst_type_exp XTs e0) m (subst_types XTs Ps)
             (List.map (subst_type_exp XTs) es)
    | e_new C es => e_new (subst_type XTs C) 
                          (List.map (subst_type_exp XTs) es)
  end.

(** * Evaluation *)

(** ** Evaluation contexts *)
(** We model evaluation contexts as functions of type [exp -> exp]. [exp_context EE] holds if [EE] is an evaluation context. Basically, any subexpression of an expression is an evaluation context. **)

Inductive exps_context : (exp -> list exp) -> Prop :=
| esc_head : forall es,
    exps_context (fun e => e::es)
| esc_tail : forall e EE,
    exps_context EE ->
    exps_context (fun e0 => e::(EE e0)).

Inductive exp_context : (exp -> exp) -> Prop :=
| ec_field_arg0 : forall f,
    exp_context (fun e0 => e_field e0 f)
| ec_meth_arg0 : forall m es fms,
    exp_context (fun e0 => e_meth e0 m fms es)
| ec_meth_args : forall m e0 fms EE,
    exps_context EE ->
    exp_context (fun e => e_meth e0 m fms (EE e))
| ec_new_args : forall C EE,
    exps_context EE ->
    exp_context (fun e => e_new C (EE e)).

Hint Constructors exp_context exps_context.

(** ** Evaluation *)
(** [eval e e'] holds when term expression [e] reduces to [e'] in one step.*)
Inductive eval : exp -> exp -> Prop :=
| eval_field : forall C fs es f e fes,
    fields C fs ->
    env_zip fs es fes ->
    binds f e fes ->
    eval (e_field (e_new C es) f) e
| eval_meth : forall C m E e e' es ves es0 t tenv Ps XTs,
    method m C E t tenv e ->
    env_zip tenv es ves ->
    env_zip E Ps XTs ->
    subst_type_exp XTs e = e' ->
    eval (e_meth (e_new C es0) m Ps es) 
         (subst_exp ((this,(e_new C es0))::ves) e')
| eval_context : forall EE e e',
    eval e e' ->
    exp_context EE ->
    eval (EE e) (EE e').

Hint Constructors eval.

(* Help Coq to eapply eval_context rule 
   ("Meta cannot occur in evar body") *)
Hint Extern 2 (eval (e_field _ ?f) _) => 
eapply (eval_context (fun e0 => e_field e0 f)).
Hint Extern 2 (eval (e_meth _ ?m ?es) _) => 
eapply (eval_context (fun e0 => e_meth e0 m es)).
Hint Extern 2 (eval (e_meth ?e0 ?m (?EE _)) _) => 
eapply (eval_context (fun e => e_meth e0 m (EE e))).
Hint Extern 2 (eval (e_new ?C (?EE _)) _) => 
eapply (eval_context (fun e => e_new C (EE e))).

(** ** Term expression typing *)

(* Auxiliary functionality *)
Inductive eval_bound : benv -> type -> type -> Prop :=
| be1 : forall env A,
    typeis_qcname A ->
    eval_bound env A A
| be2 : forall env X C,
    binds X C env ->
    eval_bound env (t_X X) (t_C C)
| be3 : forall env X C D,
    binds X D env ->
    eval_bound env (t_XdotC X C) (t_CdotC D C).

Hint Constructors eval_bound.

Definition at_exp := (type * type)%type.

(* eval_at (T1 @ T2) = T *)
Inductive eval_at : at_exp -> type -> Prop :=
  | eat1 : forall B C D,
    eval_at (t_dotC D, t_CdotC C B) (t_CdotC C D)
  | eat2 : forall B D X,
    eval_at (t_dotC D, t_XdotC X B) (t_XdotC X D)
  | eat3 : forall C D,
    eval_at (t_dotC D, t_dotC C) (t_dotC D)
  | eat4 : forall C T,
    eval_at (t_C C,T) (t_C C)
  | eat5 : forall X T,
    eval_at (t_X X,T) (t_X X)
  | eat6 : forall C D T,
    eval_at (t_CdotC D C, T) (t_CdotC D C)
  | eat7 : forall C X T,
    eval_at (t_XdotC X C, T) (t_XdotC X C).

Hint Constructors eval_at.

(* Ts @ T0 = Ts' *)
Inductive eval_ats : list type -> type -> list type -> Prop :=
| ca_nil : forall t0,
    eval_ats nil t0 nil
| ca_cons : forall u us t0 t ts,
    eval_at (u,t0) t ->
    eval_ats us t0 ts ->
    eval_ats (u::us) t0 (t::ts).

Hint Constructors eval_ats.

Inductive thistype : type -> type -> Prop :=
| tt1 : forall C,
    thistype (t_C C) (t_C C)
| tt2 : forall C E,
    thistype (t_CdotC C E) (t_dotC E).

Hint Constructors thistype.

Inductive superclass : type -> type -> Prop :=
| sc1 : forall C D fs c ms ns,
    binds C (D,fs,c,ms,ns) CT ->
    superclass (t_C C) (t_C D)
| sc2 : forall C D E fs c ms ns,
    binds C (D,fs,c,ms,ns) CT ->
    superclass (t_CdotC C E) (t_CdotC D E).

Hint Constructors superclass.

Lemma eval_bound_qcname :
  forall E B C,
    eval_bound E B C ->
    typeis_qcname C.
Proof.
  intros E B C H.
  induction H.
  assumption.
  eauto.
  eauto.
Qed.

(* Auxiliary functionality *)
Definition sub' (E:benv) (X:tvname) (C:scname) : Prop :=
  sub E (t_X X) (t_C C).

Hint Unfold sub'.

Definition scnames2types (Cs:list scname) : list type :=
  List.map (fun (C:scname) => (t_C C)) Cs.

Hint Unfold scnames2types.

Definition XClist2Xlist (l:list (tvname * scname)) : list type :=
  List.map (fun (ts:(tvname * scname)) =>
              match ts with (X,C) => t_X X end) l.

Hint Unfold XClist2Xlist.

Fixpoint ok_types (E:benv) (ts:list type) (A:type) : Prop :=
  match ts with
    | nil => True
    | t :: ts' => ok_type E t A /\ ok_types E ts' A
  end.

Hint Unfold ok_types.

Inductive subs : benv -> list type -> list scname -> Prop :=
| subs_nil : forall E,
    subs E nil nil
| subs_cons : forall E t ts c cs,
    sub E t (t_C c) ->
    subs E ts cs ->
    subs E (t :: ts) (c :: cs).

Hint Constructors subs.

(** [typing E tE e t A] holds when expression [e] has type [t] in bound environment [E] and type environment [tE], in context [A]. [wide_typing E tE e t A] holds when [e] has a subtype of [t]. wide_typings applies to lists of expressions and types in a similar manner. *)
Inductive typing : benv -> tenv -> exp ->
                   type -> type -> Prop :=
| t_var : forall x t E tE A,
    typeis_qcname A ->
    ok tE -> 
    binds x t tE ->
    typing E tE (e_var x) t A
| t_field : forall A B C f t T T0 E tE e0,
    typeis_qcname A ->
    field C f T ->
    eval_bound E B C ->
    eval_at (T,T0) t ->
    eval_at (T0,A) B ->
    typing E tE e0 T0 A ->
    typing E tE (e_field e0 f) t A
| t_invk : forall A Ps XPs U T0 t ts Us XCs 
                  Cs m xTs E tE B C e0 es b,
    typeis_qcname A ->
    typesare_famname Ps ->
    eval_at ((subst_type XPs U),T0) t ->
    eval_ats (subst_types XPs Us) T0 ts ->
    keys XPs = keys XCs ->
    imgs XPs = Ps ->
    imgs XCs = Cs ->
    imgs xTs = Us ->
    method m C XCs U xTs b ->
    eval_bound E B C ->
    eval_at (T0,A) B ->
    typing E tE e0 T0 A ->
    wide_typings E tE es ts A ->
    subs E Ps Cs ->
    typing E tE (e_meth e0 m Ps es) t A
| t_new : forall E fs es tE A A0 ts,
    typeis_qcname A ->
    fields A0 fs ->
    eval_ats (imgs fs) A0 ts ->
    wide_typings E tE es ts A ->
    typing E tE (e_new A0 es) A0 A
with wide_typing : benv -> tenv -> exp -> type -> type -> Prop :=
| wt_sub : forall E tE e t t' A,
    typeis_qcname A ->
    typing E tE e t A -> 
    sub E t t' -> 
    wide_typing E tE e t' A
with wide_typings : benv -> tenv -> list exp -> 
                    list type -> type -> Prop :=
| wts_nil : forall E tE A,
    typeis_qcname A ->
    ok E ->
    ok tE ->
    wide_typings E tE nil nil A
| wts_cons : forall E tE es E0 e t A,
    typeis_qcname A ->
    wide_typings E tE es E0 A ->
    wide_typing E tE e t A ->
    wide_typings E tE (e::es) (t::E0) A.

Hint Constructors typing wide_typing wide_typings.

(** ** Declaration typing *)

(* new ok_meth *)
Definition ok_meth (E:benv) (T0:type) (m:mname) (tE:tenv) 
           (e0:exp) (A:type) : Prop :=
  exists B,
    thistype A B /\
    wide_typing E ((this,B)::tE) e0 T0 A /\
    ok_type E T0 A /\
    ok_types E (imgs tE) A /\
    ok_types E (scnames2types (imgs E)) A /\
    E = nil /\ (* removes type arguments *)
    (forall D E' T0' Ts' e, (* override implication *)
       superclass A D -> 
       method m D E' T0' Ts' e ->
       E' = E /\ T0' = T0 /\ Ts' = tE).

Hint Unfold ok_meth.

Definition ok_meth' (A:type) (m:mname) (md:(benv * type * tenv * exp)) : Prop :=
  match md with (E,t,tE,e) => ok_meth E t m tE e A end.

Hint Unfold ok_meth'.

(** [ok_nclass E fs k ms C] holds when it is valid to define a nested class [E] with fields [fs], constructor k and methods [ms] in the context [C]. *)

(* class E{Ts fs; k ms} ok in C *)
Definition ok_nclass (E:scname) (fs:fenv) (k:kenv) (ms:menv) (C:scname) : Prop :=
  exists gs D,
    k = (E,(gs ++ fs)) /\
    superclass (t_C C) (t_C D) /\
    fields (t_CdotC D E) gs /\
    ok_types nil (imgs fs) (t_CdotC C E) /\
    forall_env (ok_meth' (t_CdotC C E)) ms.

Hint Unfold ok_nclass.

Definition ok_nclass' (C E:scname) (fkm_env:(fenv * kenv * menv)) : Prop :=
  match fkm_env with
    | (fs,k,ms) => ok_nclass E fs k ms C
  end.

Hint Unfold ok_nclass'.

(** [ok_tclass C D fs k ms ns] holds when it is valid to define a top class [C] with parent [D], fields [fs], constructor k, methods [ms] and nested classses [ns]. *)

(* class C < D{Ts fs; k ms ns} ok *)
Definition ok_tclass (C D:scname) (fs:fenv) 
           (k:kenv) (ms:menv) (ns:ncenv) : Prop :=
  exists A gs,
    k = (C,(gs ++ fs)) /\
    fields (t_C D) gs /\
    forall_env (ok_meth' (t_C C)) ms /\
    forall_env (ok_nclass' C) ns /\
    ok_types nil (imgs fs) (t_C C) /\
    ok_type nil (t_C D) A.

Hint Unfold ok_tclass.

Definition ok_tclass' (C:scname) (c:(scname * fenv * kenv * menv * ncenv)) : Prop :=
  match c with
    | (D,fs,k,ms,ns) => ok_tclass C D fs k ms ns
  end.

Hint Unfold ok_tclass'.

(** [ok_cenv ct] holds when [ct] is a well-formed class table (class environment). *)
Definition ok_cenv ct := 
  ok ct /\ forall_env ok_tclass' ct.

Hint Unfold ok_cenv.

(** * Properties *)

(** We conclude the definition of the calculus with a definition of the safety properties that are proven in the other parts of the development. *)

(** [value e] holds when the term expression [e] represents a value. Values are terms that consist only of [e_new] expressions. *)
Inductive value : exp -> Prop :=
| value_new : forall T es,
    typeis_qcname T ->
    (forall e, In e es -> value e) -> 
    value (e_new T es).

Hint Constructors value.

(** The following module defines the hypotheses of the safety argument. We assume that [Object] is not defined in the class table [CT] and that class table [CT] is well-formed. *)

Module Type Hyps.
    Parameter ct_noobj: no_binds Object CT.
    Parameter ok_ct: ok_cenv CT.
End Hyps.

(** Safety of the language may be demonstrated through an implementation of the following module type: given the above hypotheses, it provides the properties of preservation and progress. *)

Module Type Safety (H: Hyps).
    Parameter preservation: 
      forall E tE e e' T A,
        E = nil -> (* removes type arguments *)
        typing E tE e T A ->
        eval e e' ->
        wide_typing E tE e' T A.

    Parameter progress: forall e ae A,
        typing nil nil e ae A ->
        value e \/ (exists e', eval e e').
End Safety.

(** * Facts about environment starts here... *)
Lemma ok_type_weak:
  forall E E' T A x c,
    E' = (x,c) :: E ->
    ok E' ->
    ok_type E T A ->
    ok_type E' T A.
Proof.
  intros.
  induction H1.
                eauto.
              eauto.
            eauto.
          eauto.
        apply (wf_var _ _ C).
        rewrite H in *.
        apply binds_other.
        assumption.
        inversion H0; subst.
        unfold no_binds in H7.
        unfold binds in H1.
        unfold not.
        intro.
        rewrite H in H7.
        rewrite H7 in H1.
        discriminate.
        eauto.
      apply (wf_absfam _ _ _ D).
      assumption.
      rewrite H in *.
      apply binds_other.
      assumption.
      unfold not.
      intro.
      rewrite H4 in H0.
      inversion H0; subst.
      unfold no_binds in H9.
      unfold binds in H2.
      rewrite H2 in H9.
      discriminate.
    assumption.
  eauto.
Qed.

Lemma sub'_weak:
  forall E x c x' c',
    ok ((x',c') :: E) ->
    sub' E x c -> 
    sub' ((x',c') :: E) x c.
Proof.
  cut (forall E c x,
         sub' E x c ->
         forall E' x' c',
           E' = (x',c') :: E ->
           ok E' ->
           sub' E' x c).
    intros H E x c x' c' Hok Hsub'.
    apply (H E c x Hsub' _ x' c').
    reflexivity.
    assumption.
  intros E c x Hsub.
  unfold sub' in *.
  induction Hsub;
    intros E' x' c' HeqE' HokE'.
          apply s_refl.
        apply s_var.
        rewrite HeqE'.
        apply binds_other.
        assumption.
        rewrite HeqE' in HokE'.
        inversion HokE'; subst.
        unfold binds in H.
        unfold no_binds in H4.
        intro Heqx'X.
        subst x'.
        rewrite H4 in H.
        discriminate.
      apply (s_object E' T). 
    apply s_trans with (T:=T).
    eapply IHHsub1.
    eassumption.
    assumption.
    eapply IHHsub2.
    eassumption.
    assumption.
  eapply s_class.
  eassumption.
Qed.

Lemma forall_env_weak:
  forall (A:Type) (P Q:atom->A->Prop) (E:list (atom*A)),
    (forall x c, P x c -> Q x c) ->
    forall_env P E -> 
    forall_env Q E.
Proof.
  intros A P Q E H1 H2.
  induction H2.
  apply fa_nil.
  apply fa_cons.
  assumption.
  apply H1.
  apply H.
Qed.

Lemma ok_weak:
  forall (x:tvname) (c:scname) E,
    ok ((x,c) :: E) -> 
    ok E.
Proof.
  intros x0 c0 E0 H.
  inversion H; subst.
  assumption.
Qed.

Fact subEE :
  forall E, 
    ok E ->
    forall_env (sub' E) E.
Proof.
  intros E Hok.
  induction E.
  apply fa_nil.
  destruct a as [x c].
  apply fa_cons.
  apply forall_env_weak with (Q:=sub' ((x,c) :: E)) (P:=sub' E).
  intros.
  apply sub'_weak.
  unfold sub' in H.
  assumption.
  assumption.
  apply IHE.
  apply ok_weak in Hok.
  assumption.
  unfold sub'.
  apply s_var.
  apply binds_first.
Qed.
